Nuprl Lemma : w-onlnk-m
11,40
postcript
pdf
w
:World,
t
:
,
l
:IdLnk,
i
:Id. ||onlnk(
l
;m(
i
;
t
))||
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Lemmas
length
wf
nat
,
nat
wf
,
Id
wf
,
IdLnk
wf
,
world
wf
origin
w:World, t:
, l:IdLnk, i:Id. ||onlnk(l;m(i;t))|| 
w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))|| x:A. B(x) T